Inference at * 1 
Iof proof for Lemma fast-fib:

.....assertion..... NILNIL

  n, a, b:.
  {m:| 
  {k:.
  {(a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib(n+k))}  

latex

 by (InductionOnNat) 
CollapseTHEN (Auto') 

latex

C1: 

C1: 1. a : 
C1: 2. b : 
C1:   {m:| 
C1:   {k:.
C1:   {(a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib(0+k))} 
C2: 

C2: 1. n : 
C2: 2. 0 < n
C2: 3. a, b:.
C2: 3. {m:| 
C2: 3. {k:.
C2: 3. {(a = fib(k))
C2: 3. { ((k  0)  (b = 0))
C2: 3. { ((0 < k)  (b = fib(k - 1)))
C2: 3. { (m = fib((n - 1)+k))} 
C2: 4. a : 
C2: 5. b : 
C2:   {m:| 
C2:   {k:.
C2:   {(a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib(n+k))} 
C.

Definitions	n - m, n+m, -n, #$n, A, False, Void, i  j , {x:A| B(x)} , a < b, P  Q, x:AB(x), A  B, s = t, , x:A. B(x), t  T,
Lemmas	ge wf, nat properties, nat wf